\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$; ${\it da}$).
\-\\[0ex]update{-}spec{-}decl(${\it upd}$; ${\it ds}$)
\\[0ex]$\Rightarrow$ msg{-}spec{-}loc{-}decl(${\it snd}$; $i$; ${\it da}$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ R{-}Feasible\=\{i:l\}\+
\\[0ex](ecl{-}machine\{ecl:ut2\}($i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$))
\-\\[0ex]$\Rightarrow$ \=($\forall$$R$:es\_realizer\{i:l\}. \+
\\[0ex]($\neg$($\uparrow$R{-}has{-}loc($R$; $i$)))
\\[0ex]$\Rightarrow$ R{-}Feasible\=\{i:l\}\+
\\[0ex]($R$)
\-\\[0ex]$\Rightarrow$ l\_all(\=append(ecl{-}kinds($A$); fpf{-}domain(${\it da}$));\+
\\[0ex]Knd;
\\[0ex]$k$.(($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ \=(((source(lnk($k$)) = $i$ $\in$ Id)\+
\\[0ex]$\Rightarrow$ subtype\_rel(\=ma{-}valtype(${\it da}$; $k$);\+
\\[0ex]fpf{-}cap(R{-}da($R$; destination(lnk($k$))); Kind{-}deq; $k$; top)))
\-\\[0ex]$\wedge$ \=((destination(lnk($k$)) = $i$ $\in$ Id)\+
\\[0ex]$\Rightarrow$ subtype\_rel(\=fpf{-}cap(R{-}da($R$; source(lnk($k$))); Kind{-}deq; $k$; void);\+
\\[0ex]fpf{-}cap(${\it da}$; Kind{-}deq; $k$; void))))))
\-\-\-\-\\[0ex]$\Rightarrow$ R{-}compat\=\{i:l\}\+
\\[0ex](ecl{-}machine\{ecl:ut2\}($i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$); $R$))
\-\-
\end{tabbing}